Left Termination of the query pattern
overlap(g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 86 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 53 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 PiDPToQDPProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QDPSizeChangeProof (⇔, 0 ms)
        ↳11 YES
    ↳12 PiDP
        ↳13 PiDPToQDPProof (⇒, 0 ms)
        ↳14 QDP
        ↳15 QDPSizeChangeProof (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

Clauses:

overlap(Xs, Ys) :- ','(member(X, Xs), member(X, Ys)).
member(X1, []) :- ','(!, failure(a)).
member(X, Y) :- head(Y, X).
member(X, Y) :- ','(tail(Y, T), member(X, T)).
head([], X2).
head(.(H, X3), H).
tail([], []).
tail(.(X4, T), T).
failure(b).

Query: overlap(g,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

memberA(X1, .(X2, X3)) :- memberA(X1, X3).
pB(X1, .(X1, X2), X3) :- memberA(X1, X3).
pB(X1, .(X2, X3), X4) :- pB(X1, X3, X4).
overlapC(X1, X2) :- pB(X3, X1, X2).

Clauses:

membercA(X1, .(X1, X2)).
membercA(X1, .(X2, X3)) :- membercA(X1, X3).
qcB(X1, .(X1, X2), X3) :- membercA(X1, X3).
qcB(X1, .(X2, X3), X4) :- qcB(X1, X3, X4).

Afs:

overlapC(x1, x2)  =  overlapC(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
overlapC_in: (b,b)
pB_in: (f,b,b)
memberA_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

OVERLAPC_IN_GG(X1, X2) → U4_GG(X1, X2, pB_in_agg(X3, X1, X2))
OVERLAPC_IN_GG(X1, X2) → PB_IN_AGG(X3, X1, X2)
PB_IN_AGG(X1, .(X1, X2), X3) → U2_AGG(X1, X2, X3, memberA_in_gg(X1, X3))
PB_IN_AGG(X1, .(X1, X2), X3) → MEMBERA_IN_GG(X1, X3)
MEMBERA_IN_GG(X1, .(X2, X3)) → U1_GG(X1, X2, X3, memberA_in_gg(X1, X3))
MEMBERA_IN_GG(X1, .(X2, X3)) → MEMBERA_IN_GG(X1, X3)
PB_IN_AGG(X1, .(X2, X3), X4) → U3_AGG(X1, X2, X3, X4, pB_in_agg(X1, X3, X4))
PB_IN_AGG(X1, .(X2, X3), X4) → PB_IN_AGG(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
pB_in_agg(x1, x2, x3)  =  pB_in_agg(x2, x3)
.(x1, x2)  =  .(x1, x2)
memberA_in_gg(x1, x2)  =  memberA_in_gg(x1, x2)
OVERLAPC_IN_GG(x1, x2)  =  OVERLAPC_IN_GG(x1, x2)
U4_GG(x1, x2, x3)  =  U4_GG(x1, x2, x3)
PB_IN_AGG(x1, x2, x3)  =  PB_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4)  =  U2_AGG(x1, x2, x3, x4)
MEMBERA_IN_GG(x1, x2)  =  MEMBERA_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x1, x2, x3, x4)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

OVERLAPC_IN_GG(X1, X2) → U4_GG(X1, X2, pB_in_agg(X3, X1, X2))
OVERLAPC_IN_GG(X1, X2) → PB_IN_AGG(X3, X1, X2)
PB_IN_AGG(X1, .(X1, X2), X3) → U2_AGG(X1, X2, X3, memberA_in_gg(X1, X3))
PB_IN_AGG(X1, .(X1, X2), X3) → MEMBERA_IN_GG(X1, X3)
MEMBERA_IN_GG(X1, .(X2, X3)) → U1_GG(X1, X2, X3, memberA_in_gg(X1, X3))
MEMBERA_IN_GG(X1, .(X2, X3)) → MEMBERA_IN_GG(X1, X3)
PB_IN_AGG(X1, .(X2, X3), X4) → U3_AGG(X1, X2, X3, X4, pB_in_agg(X1, X3, X4))
PB_IN_AGG(X1, .(X2, X3), X4) → PB_IN_AGG(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
pB_in_agg(x1, x2, x3)  =  pB_in_agg(x2, x3)
.(x1, x2)  =  .(x1, x2)
memberA_in_gg(x1, x2)  =  memberA_in_gg(x1, x2)
OVERLAPC_IN_GG(x1, x2)  =  OVERLAPC_IN_GG(x1, x2)
U4_GG(x1, x2, x3)  =  U4_GG(x1, x2, x3)
PB_IN_AGG(x1, x2, x3)  =  PB_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4)  =  U2_AGG(x1, x2, x3, x4)
MEMBERA_IN_GG(x1, x2)  =  MEMBERA_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x1, x2, x3, x4)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 6 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERA_IN_GG(X1, .(X2, X3)) → MEMBERA_IN_GG(X1, X3)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEMBERA_IN_GG(X1, .(X2, X3)) → MEMBERA_IN_GG(X1, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MEMBERA_IN_GG(X1, .(X2, X3)) → MEMBERA_IN_GG(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 2

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PB_IN_AGG(X1, .(X2, X3), X4) → PB_IN_AGG(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
PB_IN_AGG(x1, x2, x3)  =  PB_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PB_IN_AGG(.(X2, X3), X4) → PB_IN_AGG(X3, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PB_IN_AGG(.(X2, X3), X4) → PB_IN_AGG(X3, X4)
    The graph contains the following edges 1 > 1, 2 >= 2

(16) YES